\begin{tabbing}
ma{-}feasible\=\{i:l\}\+
\\[0ex]($M$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=IdIdDeq$\forall$$x$$\in$dom($M$.1). $T$=$M$.1($x$) $\Rightarrow$  $T$\+
\\[0ex]\& KndKindDeq$\forall$$k$$\in$dom(($M$.2).1). $T$=($M$.2).1($k$) $\Rightarrow$  Dec($T$)
\\[0ex]\& ma{-}prob{-}da($M$)
\\[0ex]\& ma{-}frame{-}compat($M$;$M$)
\-
\end{tabbing}